Büchi-Elgot-Trakhtenbrot theorem

Theorem (Büchi-Elgot-Trakhtenbrot)

A language ($L$) of finite words is definable in monadic logic (i.e. the set of its structures $K_L$ is definable in $MSOL$) iff it is regular

Furthermore the translations are effective and thus satisfiability of monadic logic over finite words is decidable

(the theory of weak monadic second-order logic over $(\mathbb{N},<)$ is decidable, where weak means that second-order variables refer to finite sets)

See also

• Rabin's theorem
• Kleene's theorem
• weak monadic second-order logic

References

1. J. R. Büchi, “Weak Second‐Order Arithmetic and Finite Automata,” Mathematical Logic Qtrly, vol. 6, no. 1–6, pp. 66–92, Jan. 1960, doi: 10.1002/malq.19600060105.
2. C. C. Elgot, “Decision problems of finite automata design and related arithmetics,” Trans. Amer. Math. Soc., vol. 98, no. 1, pp. 21–51, 1961, doi: 10.1090/s0002-9947-1961-0139530-9.
3. Trakhtenbrot, B.A.: Finite automata and monadic second order logic (Russian). Siberian Math. J 3, 103–131 (1962)
4. T. Colcombet, “Composition with Algebra at the Background,” in Lecture Notes in Computer Science, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 391–404. doi: 10.1007/978-3-642-38536-0_34.
5. J. A. Makowsky, Lecture Notes, Topic: “Lecture 3: Disjoint unions and concatenation, Finite Automata, Regular Languages, The Büchi-Elgot-Trakhtenbrot Theorem.” 236331, Technion, Fall 2018. https://janos.cs.technion.ac.il/COURSES/236331-18/Lec-3.pdf
6. M. Avanzini, Lecture Notes, Topic: “weak monadic second-order logic (WMSO).” M1-AL, Centre Inria d’Université Côte d’Azur, 2021. https://www-sop.inria.fr/members/Martin.Avanzini/teaching/2021/AL/slides/w2.pdf
7. A. Amrane, H. Bazille, E. Clement, U. Fahrenberg, M. Fortin, and K. Ziemiański, “Büchi-Elgot-Trakhtenbrot Theorem for Higher-Dimensional Automata,” May 15, 2025, arXiv: arXiv:2505.10461. doi: 10.48550/arXiv.2505.10461.
8. https://en.wikipedia.org/wiki/Büchi–Elgot–Trakhtenbrot_theorem
9. https://cstheory.stackexchange.com/questions/54912/generalization-of-büchi-elgot-trakhtenbrot-theorem